0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 8 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 2 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇒, 9 ms)
↳32 QDP
↳33 MRRProof (⇔, 57 ms)
↳34 QDP
↳35 PisEmptyProof (⇔, 0 ms)
↳36 YES
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
T_IN_G(N) → U1_G(N, ll_in_ga(N, Xs))
T_IN_G(N) → LL_IN_GA(N, Xs)
LL_IN_GA(s(N), .(X, Xs)) → U5_GA(N, X, Xs, ll_in_ga(N, Xs))
LL_IN_GA(s(N), .(X, Xs)) → LL_IN_GA(N, Xs)
U1_G(N, ll_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Xs1))
U1_G(N, ll_out_ga(N, Xs)) → SELECT_IN_AGA(X1, Xs, Xs1)
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → U6_AGA(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
U2_G(N, select_out_aga(X1, Xs, Xs1)) → U3_G(N, ll_in_ag(M, Xs1))
U2_G(N, select_out_aga(X1, Xs, Xs1)) → LL_IN_AG(M, Xs1)
LL_IN_AG(s(N), .(X, Xs)) → U5_AG(N, X, Xs, ll_in_ag(N, Xs))
LL_IN_AG(s(N), .(X, Xs)) → LL_IN_AG(N, Xs)
U3_G(N, ll_out_ag(M, Xs1)) → U4_G(N, t_in_g(M))
U3_G(N, ll_out_ag(M, Xs1)) → T_IN_G(M)
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
T_IN_G(N) → U1_G(N, ll_in_ga(N, Xs))
T_IN_G(N) → LL_IN_GA(N, Xs)
LL_IN_GA(s(N), .(X, Xs)) → U5_GA(N, X, Xs, ll_in_ga(N, Xs))
LL_IN_GA(s(N), .(X, Xs)) → LL_IN_GA(N, Xs)
U1_G(N, ll_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Xs1))
U1_G(N, ll_out_ga(N, Xs)) → SELECT_IN_AGA(X1, Xs, Xs1)
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → U6_AGA(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
U2_G(N, select_out_aga(X1, Xs, Xs1)) → U3_G(N, ll_in_ag(M, Xs1))
U2_G(N, select_out_aga(X1, Xs, Xs1)) → LL_IN_AG(M, Xs1)
LL_IN_AG(s(N), .(X, Xs)) → U5_AG(N, X, Xs, ll_in_ag(N, Xs))
LL_IN_AG(s(N), .(X, Xs)) → LL_IN_AG(N, Xs)
U3_G(N, ll_out_ag(M, Xs1)) → U4_G(N, t_in_g(M))
U3_G(N, ll_out_ag(M, Xs1)) → T_IN_G(M)
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
LL_IN_AG(s(N), .(X, Xs)) → LL_IN_AG(N, Xs)
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
LL_IN_AG(s(N), .(X, Xs)) → LL_IN_AG(N, Xs)
LL_IN_AG(.(Xs)) → LL_IN_AG(Xs)
From the DPs we obtained the following set of size-change graphs:
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
SELECT_IN_AGA(.(Xs)) → SELECT_IN_AGA(Xs)
From the DPs we obtained the following set of size-change graphs:
LL_IN_GA(s(N), .(X, Xs)) → LL_IN_GA(N, Xs)
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
LL_IN_GA(s(N), .(X, Xs)) → LL_IN_GA(N, Xs)
LL_IN_GA(s(N)) → LL_IN_GA(N)
From the DPs we obtained the following set of size-change graphs:
U1_G(N, ll_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Xs1))
U2_G(N, select_out_aga(X1, Xs, Xs1)) → U3_G(N, ll_in_ag(M, Xs1))
U3_G(N, ll_out_ag(M, Xs1)) → T_IN_G(M)
T_IN_G(N) → U1_G(N, ll_in_ga(N, Xs))
t_in_g(N) → U1_g(N, ll_in_ga(N, Xs))
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_g(N, ll_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Xs1))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Xs1)) → U3_g(N, ll_in_ag(M, Xs1))
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U3_g(N, ll_out_ag(M, Xs1)) → U4_g(N, t_in_g(M))
t_in_g(0) → t_out_g(0)
U4_g(N, t_out_g(M)) → t_out_g(N)
U1_G(N, ll_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Xs1))
U2_G(N, select_out_aga(X1, Xs, Xs1)) → U3_G(N, ll_in_ag(M, Xs1))
U3_G(N, ll_out_ag(M, Xs1)) → T_IN_G(M)
T_IN_G(N) → U1_G(N, ll_in_ga(N, Xs))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U6_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
ll_in_ag(s(N), .(X, Xs)) → U5_ag(N, X, Xs, ll_in_ag(N, Xs))
ll_in_ag(0, []) → ll_out_ag(0, [])
ll_in_ga(s(N), .(X, Xs)) → U5_ga(N, X, Xs, ll_in_ga(N, Xs))
ll_in_ga(0, []) → ll_out_ga(0, [])
U6_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U5_ag(N, X, Xs, ll_out_ag(N, Xs)) → ll_out_ag(s(N), .(X, Xs))
U5_ga(N, X, Xs, ll_out_ga(N, Xs)) → ll_out_ga(s(N), .(X, Xs))
U1_G(ll_out_ga(Xs)) → U2_G(select_in_aga(Xs))
U2_G(select_out_aga(Xs1)) → U3_G(ll_in_ag(Xs1))
U3_G(ll_out_ag(M)) → T_IN_G(M)
T_IN_G(N) → U1_G(ll_in_ga(N))
select_in_aga(.(Xs)) → U6_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
ll_in_ag(.(Xs)) → U5_ag(ll_in_ag(Xs))
ll_in_ag([]) → ll_out_ag(0)
ll_in_ga(s(N)) → U5_ga(ll_in_ga(N))
ll_in_ga(0) → ll_out_ga([])
U6_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(ll_out_ag(N)) → ll_out_ag(s(N))
U5_ga(ll_out_ga(Xs)) → ll_out_ga(.(Xs))
select_in_aga(x0)
ll_in_ag(x0)
ll_in_ga(x0)
U6_aga(x0)
U5_ag(x0)
U5_ga(x0)
U1_G(ll_out_ga(Xs)) → U2_G(select_in_aga(Xs))
U2_G(select_out_aga(Xs1)) → U3_G(ll_in_ag(Xs1))
U3_G(ll_out_ag(M)) → T_IN_G(M)
T_IN_G(N) → U1_G(ll_in_ga(N))
select_in_aga(.(Xs)) → U6_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
ll_in_ag(.(Xs)) → U5_ag(ll_in_ag(Xs))
ll_in_ag([]) → ll_out_ag(0)
ll_in_ga(s(N)) → U5_ga(ll_in_ga(N))
ll_in_ga(0) → ll_out_ga([])
U6_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(ll_out_ag(N)) → ll_out_ag(s(N))
U5_ga(ll_out_ga(Xs)) → ll_out_ga(.(Xs))
llinag1 > TING1 > s1 > U3G1 > selectinaga1 > U6aga1 > U1G1 > llinga1 > 0 > selectoutaga1 > .1 > U5ga1 > U2G1 > U5ag1 > lloutag1 > [] > lloutga1
[]=2
0=1
select_in_aga_1=8
._1=6
U6_aga_1=6
select_out_aga_1=14
ll_in_ag_1=7
U5_ag_1=6
ll_out_ag_1=5
ll_in_ga_1=8
s_1=6
U5_ga_1=6
ll_out_ga_1=7
U1_G_1=2
U2_G_1=1
U3_G_1=7
T_IN_G_1=11
select_in_aga(x0)
ll_in_ag(x0)
ll_in_ga(x0)
U6_aga(x0)
U5_ag(x0)
U5_ga(x0)